Stanford Encyclopedia of Philosophy

Intuitionistic Logic

First published Wed Sep 1, 1999; substantive revision Wed Apr 28, 2010

Intuitionistic logic encompasses the principles of logical reasoning which were used by L. E. J. Brouwer in developing his intuitionistic mathematics, beginning in [1907]. Because these principles also underly Russian recursive analysis and the constructive analysis of E. Bishop and his followers, intuitionistic logic may be considered the logical basis of constructive mathematics.

Philosophically, intuitionism differs from logicism by treating logic as a part of mathematics rather than as the foundation of mathematics; from finitism by allowing (constructive) reasoning about infinite collections; and from platonism by viewing mathematical objects as mental constructs with no independent ideal existence. Hilbert's formalist program, to justify classical mathematics by reducing it to a formal system whose consistency should be established by finitistic (hence constructive) means, was the most powerful contemporary rival to Brouwer's developing intuitionism. In his 1912 essay Intuitionism and Formalism Brouwer correctly predicted that any attempt to prove the consistency of complete induction on the natural numbers would lead to a vicious circle.

Brouwer rejected formalism per se but admitted the potential usefulness of formulating general logical principles expressing intuitionistically correct constructions, such as modus ponens. Formal systems for intuitionistic propositional and predicate logic and arithmetic were developed by Heyting [1930], Gentzen [1935] and Kleene [1952]. Gödel [1933] proved the equiconsistency of intuitionistic and classical theories. Kripke [1965] provided a semantics with respect to which intuitionistic logic is correct and complete.

1. Rejection of Tertium Non Datur

Intuitionistic logic can be succinctly described as classical logic without the Aristotelian law of excluded middle (LEM): (A ∨ ¬A), but with the law of contradiction (¬A → (A → B)). Brouwer [1908] observed that LEM was abstracted from finite situations, then extended without justification to statements about infinite collections. For example, if x, y range over the natural numbers 0, 1, 2, … and B(x) abbreviates the property (there is a y > x such that both y and y+2 are prime numbers), then we have no general method for deciding whether B(x) is true or false for arbitrary x, so ∀x(B(x) ∨ ¬B(x)) cannot be asserted in the present state of our knowledge. And if A abbreviates the statement ∀xB(x), then (A ∨ ¬A) cannot be asserted because neither A nor (¬A) has yet been proved.

One may object that these examples depend on the fact that the Twin Primes Conjecture has not yet been settled. A number of Brouwer's original “counterexamples” depended on problems (such as Fermat's Last Theorem) which have since been solved. But to Brouwer the general LEM was equivalent to the a priori assumption that every mathematical problem has a solution — an assumption he rejected, anticipating Gödel's incompleteness theorem by a quarter of a century.

The rejection of LEM has far-reaching consequences. On the one hand,

On the other hand,

2. Intuitionistic First-Order Predicate Logic

Formalized intuitionistic logic is naturally motivated by the informal Brouwer-Heyting-Kolmogorov explication of intuitionistic truth, outlined in Section 2 of the article on Constructive Mathematics in this Encyclopedia. The constructive independence of the logical operations &, ∨, →, ¬, ∀, ∃ contrasts with the classical situation, where e.g., (A ∨ B) is equivalent to ¬(¬A & ¬B), and ∃xA(x) is equivalent to ¬∀x¬A(x). From the B-H-K viewpoint, a sentence of the form (A ∨ B) asserts that either a proof of A, or a proof of B, has been constructed; while ¬(¬A & ¬B) asserts that an algorithm has been constructed which would effectively convert any pair of constructions proving ¬A and ¬B respectively, into a proof of a known contradiction.

Following is a Hilbert-style formalism H, from Kleene [1952], for intuitionistic first-order predicate logic IQC. The language L has predicate letters P, Q(.),… of all arities and individual variables a, b, c,… (with or without subscripts 1,2,…), as well as symbols &, ∨, →, ¬, ∀, ∃ for the logical connectives and quantifiers, and parentheses (, ). The prime formulas of L are expressions such as P, Q(a), R(a, b, a) where P, Q(.), R(…) are 0-ary, 1-ary and 3-ary predicate letters respectively; that is, the result of filling each blank in a predicate letter by an individual variable symbol is a prime formula. The (well-formed) formulas of L are defined inductively as follows.

In general, we use A, B, C as metavariables for well-formed formulas and x, y, z as metavariables for individual variables. Anticipating applications (for example to intuitionistic arithmetic) we use s, t as metavariables for terms; in the case of pure predicate logic, terms are simply individual variables. An occurrence of a variable x in a formula A is bound if it is within the scope of a quantifier ∀x or ∃x, otherwise free. Intuitionistically as classically, “(A ↔ B)” abbreviates “(A → B) & (B → A),” and parentheses are omitted when this causes no confusion.

There are three rules of inference:

The axioms are all formulas of the following forms, where in the last two schemas the subformula A(t) is the result of substituting an occurrence of the term t for every free occurrence of x in A(x), and no variable free in t becomes bound in A(t) as a result of the substitution.

A proof is any finite sequence of formulas, each of which is an axiom or an immediate consequence, by a rule of inference, of (one or two) preceding formulas of the sequence. Any proof is said to prove its last formula, which is called a theorem or provable formula of first-order intuitionistic predicate logic. A derivation of a formula E from a collection F of assumptions is any sequence of formulas, each of which belongs to F or is an axiom or an immediate consequence, by a rule of inference, of preceding formulas of the sequence, such that E is the last formula of the sequence. If such a derivation exists, we say E is derivable from F.

Intuitionistic propositional logic IPC is the subtheory which results when the language is restricted to formulas built from proposition letters P, Q, R,… using the propositional connectives &, ∨, → and ¬, and only the propositional postulates are used. Thus the last two rules of inference and the last two axiom schemas are absent from the propositional theory.

If, in the given list of axiom schemas for intuitionistic propositional or first-order predicate logic, the law of contradiction:

¬A → (A → B).

is replaced by the law of double negation:

¬ ¬A → A.

(or,equivalently, by LEM), a formal system for classical propositional logic CPC or classical predicate logic CQC results. Since the law of contradiction is a classical theorem, intuitionistic logic is contained in classical logic. In a sense, classical logic is also contained in intuitionistic logic; see Section 4.1 below.

It is important to note that while LEM and the law of double negation are equivalent as schemas, the implication (¬ ¬A → A) → (A ∨ ¬A) is not a theorem schema of IPC. For theories T based on intuitionistic logic, if E is an arbitrary formula of L(T) then by definition

Decidability implies stability, but not conversely. By Brouwer's first published logical theorem ¬ ¬ ¬A → ¬A, every formula of the form ¬A is stable; but in IPC and IQC prime formulas and their negations are undecidable, as shown in Section 5.1 below.

The Hilbert-style system H is useful for metamathematical investigations of intuitionistic logic, but its forced linearization of deductions and its preference for axioms over rules make it an awkward instrument for establishing derivability. A natural deduction system I for intuitionistic predicate logic results from the deductive system D, presented in Section 3 of the entry on Classical Logic in this Encyclopedia, by omitting the symbol and rules for identity, and replacing the classical rule (DNE) of double negation elimination by the intuitionistic negation elimination rule

(INE) If F entails A and F entails ¬A, then F entails B.

While identity can of course be added to intuitionistic logic, for applications (e.g., to arithmetic) the equality symbol is generally treated as a distinguished predicate constant satisfying nonlogical axioms (e.g., the primitive recursive definitions of addition and multiplication) in addition to reflexivity, symmetry and transitivity. Identity is decidable, intuitionistically as well as classically, but intuitionistic extensional equality is not always decidable; see the discussion of Brouwer's continuum in the article on Constructive Mathematics in this Encyclopedia. The keys to proving that H is equivalent to I are modus ponens and its converse, the

Deduction Theorem: If B is derivable from A and possibly other formulas F, with all variables free in A held constant in the derivation (that is, without using the second or third rule of inference on any variable x occurring free in A, unless the assumption A does not occur in the derivation before the inference in question), then (A → B) is derivable from F.

This fundamental result, roughly expressing the rule (→I) of I, can be proved for H by induction on the definition of a derivation. The other rules of I hold for H essentially by modus ponens, which corresponds to (→E) in I. To illustrate the usefulness of the Deduction Theorem, consider the (apparently trivial) theorem schema (A → A) of IPC. A correct proof in H takes five lines:

1. A → (A → A)
2. (A → (A → A)) → ((A → ((A → A) → A)) → (A → A))
3. (A → ((A → A) → A)) → (A → A)
4. A → ((A → A) → A)
5. A → A

where 1, 2 and 4 are axioms and 3, 5 come from earlier lines by modus ponens. However, A is derivable from A (as assumption) in one obvious step, so the Deduction Theorem allows us to conclude that a proof of (A → A) exists. (In fact, the formal proof of (A → A) just presented is part of the constructive proof of the Deduction Theorem!)

It is important to note that, in the definition of a derivation from assumptions in H, the assumption formulas are treated as if all their free variables were universally quantified, so that ∀x A(x) is derivable from the hypothesis A(x). However, the variable x will be varied (not held constant) in that derivation, by use of the rule of ∀-introduction; and so the Deduction Theorem cannot be used to conclude (falsely) that A(x) → ∀x A(x) (and hence, by ∃-elimination, ∃x A(x) → ∀x A(x)) are provable in H. As an example of a correct use of the Deduction Theorem for predicate logic, consider the implication ∃x A(x) → ¬∀x¬A(x). To show this is provable in IQC, we first derive ¬∀x¬A(x) from A(x) with all free variables held constant:

1. ∀x¬A(x) → ¬A(x)
2. A(x) → (∀x¬A(x) → A(x))
3. A(x) (assumption)
4. ∀x¬A(x) → A(x)
5. (∀x¬A(x) → A(x)) → ((∀x¬A(x) → ¬A(x)) → ¬∀x¬A(x))
6. (∀x¬A(x) → ¬A(x)) → ¬∀x¬A(x)
7. ¬∀x¬A(x))

Here 1, 2 and 5 are axioms; 4 comes from 2 and 3 by modus ponens; and 6 and 7 come from earlier lines by modus ponens; so no variables have been varied. The Deduction Theorem tells us there is a proof P in IQC of (A(x) → ¬∀x¬A(x)), and one application of ∃-introduction converts P into a proof of ∃x A(x) → ¬∀x¬A(x). The converse is not provable in IQC, as shown in Section 5.1 below.

3. Intuitionistic Number Theory (Heyting Arithmetic)

Intuitionistic (Heyting) arithmetic HA and classical (Peano) arithmetic PA share the same first-order language and the same non-logical axioms; only the logic is different. In addition to the logical connectives, quantifiers and parentheses and the individual variables a, b, c, … (with metavariables x, y, z as usual), the language L(HA) of arithmetic has a binary predicate symbol =, individual constant 0, unary function constant S, and finitely or countably infinitely many additional constants for primitive recursive functions including addition and multiplication; the precise choice is a matter of taste and convenience. Terms are built from variables and 0 using the function constants; in particular, each natural number n is expressed in the language by the numeral n obtained by applying S n times to 0 (e.g., S(S(0)) is the numeral for 2). Prime formulas are of the form (s = t) where s, t are terms, and compound formulas are obtained from these as usual.

The logical axioms and rules of HA are those of first-order intuitionistic predicate logic IQC. The nonlogical axioms include the reflexive, symmetric and transitive properties of =, primitive recursive defining equations for each function constant, the axioms characterizing 0 as the least natural number and S as a one-to-one function:

the extensional equality axiom for S:

and the (universal closure of the) schema of mathematical induction, for arbitrary formulas A(x):

Extensional equality axioms for all the other function constants are derivable by mathematical induction from the equality axiom for S and the primitive recursive function axioms.

The natural order relation x < y can be defined in HA by ∃z(S(z) + x = y), or by a quantifier-free formula if the symbol and defining axioms for cutoff subtraction are present in the formalism. HA proves the comparative law

∀x ∀y (x < y ∨ x = y ∨ y < x)

and an intuitionistic form of the least number principle, for arbitrary formulas A(x):

∀x[∀y (y < x → A(y) ∨ ¬A(y)) → ∃y (y < x & A(y) & ∀z(z < y → ¬A(z))) ∨ ∀y(y < x → ¬A(y))].

The hypothesis is needed because not all arithmetical formulas are decidable in HA. However, ∀x∀y(x = y ∨ ¬(x = y)) can be proved directly by mathematical induction, and so

  • Prime formulas (and hence all quantifier-free formulas) are decidable and stable in HA.

If A(x) is decidable in HA, then by induction on x so are ∀y (y < x → A(y)) and ∃y (y < x & A(y)). Hence

  • Formulas in which all quantifiers are bounded are decidable and stable in HA.

The collection Δ0 of arithmetical formulas in which all quantifiers are bounded is the lowest level of a classical arithmetical hierarchy based on the pattern of alternations of quantifiers in a prenex formula. In HA not every formula has a prenex form, but Burr [2004] discovered a simple intuitionistic arithmetical hierarchy corresponding level by level to the classical. For the purposes of the next two definitions only, ∀x denotes a block of finitely many universal number quantifiers, and similarly ∃x denotes a block of finitely many existential number quantifiers. With these conventions, Burr's classes Φn and Ψn are defined by

The corresponding classical prenex classes are defined more simply:

Peano arithmetic PA comes from Heyting arithmetic HA by adding LEM or (¬ ¬A → A) to the list of logical axioms, i.e., by using classical instead of intuitionistic logic. The following results hold even in the fragments of HA and PA with the induction schema restricted to Δ0 formulas.

Burr's Theorem:
  • Every arithmetical formula is provably equivalent in HA to a formula in one of the classes Φn.
  • Every formula in Φn is provably equivalent in PA to a formula in Πn, and conversely.
  • Every formula in Ψn is provably equivalent in PA to a formula in Σn, and conversely.

HA and PA are proof-theoretically equivalent, as will be shown in Section 4. Each is capable of (numeralwise) expressing its own proof predicate. By Gödel's famous Incompleteness Theorem, if HA is consistent then neither HA nor PA can prove its own consistency.

4. Basic Proof Theory

4.1 Translating classical into intuitionistic logic

A fundamental fact about intuitionistic logic is that it has the same consistency strength as classical logic. For propositional logic this was first proved by Glivenko [1929].

Glivenko's Theorem: An arbitrary propositional formula A is classically provable, if and only if ¬¬A is intuitionistically provable.

Glivenko's Theorem does not extend to predicate logic, although an arbitrary predicate formula A is classically provable if and only if ¬¬A is provable in intuitionistic predicate logic plus the “double negation shift” schema

(DNS) ∀x¬¬B(x) → ¬¬∀x B(x).

The more sophisticated negative translation of classical into intuitionistic theories, due independently to Gödel and Gentzen, associates with each formula A of the language L another formula g(A) (with no ∨ or ∃), such that

(I) Classical predicate logic proves A ↔ g(A).
(II) Intuitionistic predicate logic proves g(A) ↔ ¬¬g(A).
(III) If classical predicate logic proves A, then intuitionistic predicate logic proves g(A).

The proofs are straightforward from the following inductive definition of g(A) (using Gentzen's direct translation of implication, rather than Gödel's in terms of ¬ and &):

For each formlula A, g(A) is provable intuitionistically if and only if A is provable classically. In particular, if (B & ¬B) were classically provable for some formula B, then (g(B) & ¬g(B)) (which is g(B & ¬B)) would in turn be provable intuitionistically. Hence

(IV) Classical and intuitionistic predicate logic are equiconsistent.

The negative translation of classical into intuitionistic number theory is even simpler, since prime formulas of intuitionistic arithmetic are stable. Thus g(s=t) can be taken to be (s=t), and the other clauses are unchanged. The negative translation of any instance of mathematical induction is another instance of mathematical induction, and the other nonlogical axioms of arithmetic are their own negative translations, so

(I), (II), (III) and (IV) hold also for number theory.

Gödel [1933] interpreted these results as showing that intuitionistic logic and arithmetic are richer than classical logic and arithmetic, because the intuitionistic theory distinguishes formulas which are classically equivalent, and has the same consistency strength as the classical theory.

Direct attempts to extend the negative interpretation to analysis fail because the negative translation of the countable axiom of choice is not a theorem of intuitionistic analysis. However, it is consistent with intuitionistic analysis, including Brouwer's controversial continuity principle, by the functional version of Kleene's recursive realizability (Section 5.2 below).

4.2 Admissible rules of intuitionistic logic

Gödel [1932] observed that intuitionistic propositional logic has the disjunction property:

(DP) If (A ∨ B) is a theorem, then A is a theorem or B is a theorem.

Gentzen [1935] established the disjunction property for closed formulas of intuitionistic predicate logic. From this it follows that if intuitionistic logic is consistent, then (P ∨ ¬P) is not a theorem if P is prime. Kleene [1945, 1952] proved that intuitionistic first-order number theory also has the related (cf. Friedman [1975]) existence property:

(ED) If ∃xA(x) is a closed theorem, then for some closed term t, A(t) is a theorem.

The disjunction and existence properties are special cases of a general phenomenon peculiar to nonclassical theories. The admissible rules of a theory are the rules under which the theory is closed. For example, Harrop [1960] observed that the rule

If (¬A → (B ∨ C)) is a theorem, so is (¬A → B) ∨ (¬A → C)

is admissible for intuitionistic propositional logic IPC because if A, B and C are any formulas such that (¬A → (B ∨ C)) is provable in IPC, then also (¬A → B) ∨ (¬A → C) is provable in IPC. Harrop's rule is not derivable in IPC because (¬A → (B ∨ C)) → (¬A → B) ∨ (¬A → C) is not intuitionistically provable. Another important example of an admissible nonderivable rule of IPC is Mints' rule:

If ((A → B) → A ∨ C) is a theorem, so is ((A → B) → A) ∨ ((A → B) → C).

The two-valued truth table interpretation of classical propositional logic CPC gives rise to a simple proof that every admissible rule of CPC is derivable: otherwise, some assignment to A, B, etc. would make the hypothesis true and the conclusion false, and by substituting e.g. (P → P) for the letters assigned “true” and (P & ¬ P) for those assigned “false” one would have a provable hypothesis and unprovable conclusion. The fact that the intuitionistic situation is more interesting leads to many natural questions, some of which have recently been answered.

By generalizing Mints' Rule, Visser and de Jongh identified a recursively enumerable sequence of successively stronger admissible rules (“Visser's rules”) which, they conjectured, formed a basis for the admissible rules of IPC in the sense that every admissible rule is derivable from the disjunction property and one of the rules of the sequence. Building on work of Ghilardi [1999], Iemhoff [2001] succeeded in proving their conjecture. Rybakov [1997] proved that the collection of all admissible rules of IPC is decidable but has no finite basis. Visser [2002] showed that his rules are also the admissible propositional rules of HA, and of HA extended by Markov's Principle MP (defined in Section 5.1 below). More recently, Jerabek [2008] found a different basis for the admissible rules of IPC with the property that no rule in the basis derives another.

An intermediate propositional logic is any consistent collection of propositional formulas containing all the axioms of IPC and closed under modus ponens and substitution of arbitrary formulas for proposition letters. Each intermediate propositional logic is contained in CPC. Gödel [1933] used an infinite sequence of successively stronger intermediate logics to show that IPC has no finite truth-table interpretation. Iemhoff [2005] proved that IPC is the only intermediate logic with the disjunction property which is closed under all the Visser rules. Iemhoff and Metcalfe [2009] developed a formal calculus for generalized admissibility for IPC and some intermediate logics.

While the admissible rules of intuitionistic predicate logic have not been completely characterized, they are known to include Markov's Rule for decidable predicates:

If ∀x(A(x) ∨ ¬A(x)) & ¬∀x¬A(x) is a theorem, so is ∃x A(x)

and the following Independence-of-Premise Rule (where y is assumed not to occur free in A(x)):

If ∀x(A(x) ∨ ¬A(x)) & (∀x A(x) → ∃y B(y)) is a theorem, so is ∃y (∀x A(x) → B(y)).

The corresponding implications (MP and IP respectively), which are not provable intuitionistically, are verified by Gödel's “Dialectica” interpretation of HA (cf. Section 6 below). So is the implication (CT) corresponding to one of the most interesting admissible rules of Heyting arithmetic, let us call it the Church-Kleene Rule:

If ∀x ∃y A(x, y) is a closed theorem of HA then there is a number n such that, provably in HA, the partial recursive function with Gödel number n is total and maps each x to a y satisfying A(x, y) (and moreover A(x,y) is provable, where x is the numeral for the natural number x and y is the numeral for y).

Combining Markov's Rule with the negative translation gives the result that classical and intuitionistic arithmetic prove the same formulas of the form ∀x ∃y A(x, y) where A(x, y) is quantifier-free. In general, if A(x, y) is provably decidable in HA and if ∀x ∃y A(x, y) is a closed theorem of classical arithmetic, the conclusion of the Church-Kleene Rule holds even in intuitionistic arithmetic.

Here is a proof that the rule “If ∀x (A ∨ B(x)) is a theorem, so is A ∨ ∀x B(x)” (where x is not free in A) is not admissible for HA, if HA is consistent. Gödel numbering provides a quantifier-free formula G(x) which (numeralwise) expresses the predicate “x is the code of a proof in HA of (0 = 1).” By intuitionistic logic with the decidability of quantifier-free arithmetical formulas, HA proves ∀x(∃yG(y) ∨ ¬G(x)). However, if HA proved ∃yG(y) ∨ ∀x¬G(x) then by the disjunction property, HA must prove either ∃yG(y) or ∀x¬G(x). The first case is impossible, by the existence property with the consistency assumption and the fact that HA proves all true quantifier-free sentences. But the second case is also impossible, by Gödel's second incompleteness theorem, since ∀x¬G(x) expresses the consistency of HA.

5. Basic Semantics

5.1 Kripke semantics for intuitionistic logic

Intuitionistic systems have inspired a variety of interpretations, including Beth's tableaus, Rasiowa and Sikorski's topological models, formulas-as-types, Kleene's recursive realizabilities, and the Kleene and Aczel slashes. Kripke's [1965] possible-world semantics, with respect to which intuitionistic predicate logic is complete and consistent, most resembles classical model theory.

A Kripke structure K for L consists of a partially ordered set K of nodes and a domain function D assigning to each node k in K an inhabited set D(k), such that if k ≤ k′, then D(k) ⊆ D(k′). In addition K has a forcing relation determined as follows.

For each node k let L(k) be the language extending L by new constants for all the elements of D(k). To each node k and each 0-ary predicate letter (each proposition letter) P, either assign f(P, k) = true or leave f(P, k) undefined, consistent with the requirement that if k ≤ k′ and f(P, k) = true then f(P, k′) = true also. Say that

k forces P if and only if f(P, k) = true.

To each node k and each (n+1)-ary predicate letter Q(…), assign a (possibly empty) set T(Q, k) of (n+1)-tuples of elements of D(k) in such a way that if k ≤ k′ then T(Q, k) ⊆ T(Q, k′). Say that

k forces Q(d0,…,dn) if and only if (do,…,dn) ∈ T(Q, k).

Now define forcing for compound sentences of L(k) inductively as follows:

Any such forcing relation is consistent and monotone:

Kripke's Soundness and Completeness Theorems establish that a sentence of L is provable in intuitionistic predicate logic if and only if it is forced by every node of every Kripke structure. Thus to show that (¬∀x¬P(x) → ∃xP(x)) is intuitionistically unprovable, it is enough to consider a Kripke structure with K = {k, k′}, k < k′, D(k) = D(k′) = {0}, T(P, k) empty but T(P, k′) = {0}. And to show the converse is intuitionistically provable (without actually exhibiting a proof), one only needs the consistency and monotonicity properties of arbitrary Kripke models, with the definition of forcing.

Kripke models for languages with equality may interpret = at each node by an arbitrary equivalence relation, subject to monotonicity. For applications to intuitionistic arithmetic, normal models (those in which equality is interpreted by identity at each node) suffice because equality of natural numbers is decidable.

Propositional Kripke semantics is particulary simple, since an arbitrary propositional formula is intuitionistically provable if and only if it is forced by the root of every Kripke model whose frame (the set K of nodes together with their partial ordering) is a finite tree with a least element (the root). For example, the Kripke model with K = {k, k′, k ′′}, k < k′ and k < k′′, and with P true only at k′, shows that both P ∨ ¬P and ¬P ∨ ¬¬P are unprovable in IPC.

Each terminal node or leaf of a Kripke model is a classical model, because a leaf forces every formula or its negation. Only those proposition letters which occur in a formula E, and only those nodes k′ such that k≤k′, are relevant to deciding whether or not k forces E. Such considerations allow us to associate effectively with each formula E of L(IPC) a finite class of finite Kripke structures which will include a countermodel to E if one exists. Since the class of all theorems of IPC is recursively enumerable, we conclude that

IPC is effectively decidable. There is a recursive procedure which determines, for each propositional formula E, whether or not E is a theorem of IPC, concluding with either a proof of E or a Kripke countermodel.

The decidability of IPC was first obtained by Gentzen in 1933 as an immediate corollary of his Hauptsatz. The undecidability of IQC follows from the undecidability of CQC by the negative interpretation.

Familiar non-intuitionistic logical schemata correspond to structural properties of Kripke models, for example

Kripke models are a powerful tool for establishing properties of intuitionistic formal systems; cf. Troelstra and van Dalen [1988], Smorynski [1973], de Jongh and Smorynski [1976], Ghilardi [1999] and Iemhoff [2001], [2005]. Following Gödel, Kreisel [1962] argued that Kripke-completeness of intuitionistic logic entailed Markov's Principle. By modifying the definition of a Kripke model to allow “exploding nodes” which force every sentence, Veldman [1976] found an intuitionistic completeness proof avoiding (the informal use of) MP.

5.2 Realizability semantics for Heyting arithmetic

One way to implement the B-H-K explication of intuitionistic truth for arithmetic is to associate with each sentence E of HA some collection of numerical codes for algorithms which could establish the constructive truth of E. Following Kleene [1945], a number e realizes a sentence E of the language of arithmetic by induction on the logical form of E:

An arbitrary formula is realizable if some number realizes its universal closure. Observe that not both A and ¬A are realizable, for any formula A. The fundamental result is

Nelson's Theorem [1947]. If A is derivable in HA from realizable formulas F, then A is realizable.

Some nonintuitionistic principles can be shown to be realizable. For example, Markov's Principle (for decidable formulas) can be expressed by the schema

(MP) ∀x(A(x) ∨ ¬A(x)) & ¬∀x¬A(x) → ∃x A(x).

MP is realizable by an argument which uses Markov's Principle informally. But realizability is a fundamentally nonclassical interpretation. In HA it is possible to express an axiom of recursive choice CT (for “Church's Thesis”), which contradicts LEM but is (constructively) realizable. Hence by Nelson's Theorem, HA + MP + CT is consistent.

Kleene used a variant of number-realizability to prove HA satisfies the Church-Kleene Rule; the same argument works for HA with MP and/or CT. In Kleene and Vesley [1965] and Kleene [1969], functions replace numbers as realizing objects, establishing the consistency of formalized intuitionistic analysis and its closure under a second-order version of the Church-Kleene Rule.

De Jongh [1970] combined realizability with Kripke modeling to show that intuitionistic predicate logic is arithmetically complete for HA. If, to each n-place predicate letter P(…), a formula f(P) of L(HA) with n free variables is assigned, and if the formula f(A) of L(HA) comes from the formula A of L by replacing each prime formula P(x1,…, xn) by f(P)(x1,…, xn), then f(A) is called an arithmetical substitution instance of A. A uniform assignment of simple existential formulas to predicate letters suffices to prove

De Jongh's Theorem. If a sentence A of the language L is not provable in IQC, then some arithmetical substitution instance of A is not provable in HA.

For example, if P(x, y) expresses “x codes a proof in HA of the formula with code y,” then ∀y (∃x P(x, y) ∨ ¬∃x P(x, y)) is unrealizable, hence unprovable in HA, and so is its double negation. (The proof of de Jongh's Theorem for IPC does not need realizability; cf. Smorynski [1973]. For example, Rosser's form of Gödel's Incompleteness Theorem provides a sentence C of L(HA) such that PA proves neither C nor ¬C, so by the disjunction property HA cannot prove (C ∨ ¬C).)

Without claiming that number-realizability coincides with intuitionistic arithmetical truth, Nelson observed that for each formula A of L(HA) the predicate “y realizes A” can be expressed in HA by another formula (abbreviated “y re A”), and the schema A ↔ ∃y (y re A) is consistent with HA. Troelstra [1973] showed that HA + (A ↔ ∃y (y re A)) is equivalent to HA + ECT, where ECT is a strengthened form of CT. In HA + MP + ECT, which Troelstra considers to be a formalization of Russian recursive mathematics (RUSS in the article on Constructive Mathematics in this Encyclopedia), every formula of the form (y re A) has an equivalent “classical” prenex form A′(y) consisting of a quantifier-free subformula preceded by alternating “classical” quantifiers of the forms ¬¬∃x and ∀z¬¬, and so ∃y A′(y) is a kind of prenex form of A.

While HA is a proper part of classical arithmetic, the intuitionistic attitude toward mathematical objects results in a theory of real numbers (INT in the article on Constructive Mathematics) diverging from the classical. Kleene's function-realizability, developed to prove the consistency of INT, changes the interpretation of arithmetical formulas. For example, ¬¬∀x (A(x) ∨ ¬A(x)) is function-realizable for every arithmetical formula A(x). In the language of analysis, Markov's Principle and the negative translation of the countable axiom of choice are among the many non-intuitionistic principles which are function-realizable (by classical arguments) and hence consistent with INT; cf. Kleene [1965], Vesley [1972] and Moschovakis [2003]. Abstract and concrete realizability semantics for a wide variety of formal systems have been developed and studied by logicians and computer scientists; cf. Troelstra [1998] and van Oosten [2002] and [2008]. Variations of the basic notions are useful for establishing relative independence of the nonlogical axioms in theories based on intuitionistic logic.

6. Advanced Topics and Recommended Reading

The article on L. E. J. Brouwer in this Encyclopedia discusses Brouwer's philosophy and mathematics, with a chronology of his life and a selected list of publications including translations and secondary sources. The best way to learn more is to read some of the original papers. English translations of Brouwer's doctoral dissertation and other papers which originally appeared in Dutch, along with a number of articles in German, can be found in L. E. J. Brouwer: Collected Works [1975], edited by Heyting. Benacerraf and Putnam's essential source book contains Brouwer [1912] (in English translation), Brouwer [1949] and Dummett [1975]. Mancosu's [1998] provides English translations of many fundamental articles by Brouwer, Heyting, Glivenko and Kolmogorov, with illuminating introductory material by W. van Stigt whose [1990] is another valuable resource.

The third edition [1971] of Heyting's classic [1956] is an attractive introduction to intuitionistic philosophy, logic and mathematical practice. As part of the formidable project of editing and publishing Brouwer's Nachlass, van Dalen [1981] provides a comprehensive view of Brouwer's own intuitionistic philosophy. The English translation, in van Heijenoort [1969], of Brouwer's [1927] (with a fine introduction by Parsons) is still an indispensable reference for Brouwer's theory of the continuum. Veldman [1990] and [2005] are authentic modern examples of traditional intuitionistic mathematical practice. Troelstra [1991] places intuitionistic logic in its historical context as the common foundation of constructive mathematics in the twentieth century.

Kleene and Vesley's [1965] gives a careful axiomatic treatment of intuitionistic analysis, a proof of its consistency relative to a classically correct subtheory, and an extended application to Brouwer's theory of real number generators. Kleene's [1969] formalizes the theory of partial recursive functionals, enabling precise formalizations of the function-realizability interpretation used in [1965] and of a related q-realizability interpretation which gives the Church-Kleene Rule for intuitionistic analysis.

An alternative to realizability semantics for intuitionistic arithmetic is Gödel's [1958] “Dialectica” interpretation, which associates with each formula B of L(HA) a quantifier-free formula BD in the language of intuitionistic arithmetic of all finite types. The “Dialectica” interpretation of B, call it BD, is ∃Y∀x BD(Y, x). If B is a closed theorem of HA, then BD(F, x) is provable for some term F in Gödel's theory T of “primitive recursive” functionals of higher type. The translation from B to BD requires the axiom of choice (at all finite types), MP and IP, so is not strictly constructive; however, the number-theoretic functions expressible by terms F of T are precisely the provably recursive functions of HA (and of PA). The interpretation was extended to analysis by Spector [1962]; cf. Howard [1973]. Clear expositions, and additional references, are to be found in Troelstra's introduction to the English translation in Gödel [1990] of the original Dialectica article, and in Avigad and Feferman [1998].

Another line of research in intuitionistic logic concerns Brouwer's very controversial “creating subject counterexamples” to principles of classical analysis (such as Markov's Principle) which could not be refuted on the basis of the theory FIM of Kleene and Vesley [1965]. By weakening Kleene's form of Brouwer's principle of continuous choice, and adding an axiom he called Kripke's Schema (KP), Myhill managed to formalize the creating subject arguments. KP is inconsistent with FIM, but Vesley found an alternative principle (Vesley's Schema (VS)) which can consistently be added to FIM and implies all the counterexamples for which Brouwer required a creating subject. Krol and Scowcroft gave topological consistency proofs for intuitionistic analysis with Kripke's Schema and weak continuity.

Troelstra's [1973], Beeson's [1985] and Troelstra and van Dalen's [1988] stand out as the most comprehensive studies of intuitionistic and semi-intutionistic formal theories, using both constructive and classical methods, with useful bibliographies. Troelstra's [1998] presents formulas-as-types and (Kleene and Aczel) slash interpretations for propositional and predicate logic, as well as abstract and concrete realizabilities for a multitude of applications. Martin-Löf's constructive theory of types [1984] (cf. Section 3.4 of Constructive Mathematics) provides a general framework within which intuitionistic reasoning continues to develop.

Bibliography

Other Internet Resources

Related Entries

Brouwer, Luitzen Egbertus Jan | Gödel, Kurt | logic-history-of | logic: classical | logic: provability | mathematics, philosophy of: formalism | mathematics-philosophy-of | mathematics: constructive | platonism-in-metaphysics